\begin{tabbing}
World
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$T$:(Id$\rightarrow$Id$\rightarrow$Type)\+
\\[0ex]$\times$ (${\it TA}$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ $s$:($i$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow\mathbb{Q}\rightarrow$$T$($i$,$x$)))
\\[0ex]$\times$ $a$:($i$:Id$\rightarrow\mathbb{N}\rightarrow$Action(w{-}action{-}dec(${\it TA}$;$M$;$i$)))
\\[0ex]$\times$ $m$:($i$:Id$\rightarrow\mathbb{N}\rightarrow$(\{$m$:Msg($M$)$\mid$ source(mlnk($m$)) = $i$\}  List))
\\[0ex]$\times$ :($i$:Id$\rightarrow$w{-}automaton($T$($i$);${\it TA}$($i$);$M$))
\\[0ex]$\times$ (${\it discrete}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$)
\\[0ex]$\times$ Top))
\-
\end{tabbing}